x, y:Atom2. x =a2 y  x = y 

latex

Definitions	P  Q, P & Q, P  Q, P  Q, eq_atom$n(x;y), x:A. B(x), b, Prop, s = t, Type, Atom$n, t  T, b, Dec(P), P  Q, left+right, , false, A, False, x:AB(x), x:AB(x), true
Lemmas	btrue wf, eqtt to assert, assert of bnot, bfalse wf, eqff to assert, decidable atom equal 2, eq atom wf2, assert wf